package edu.cmu.cs.erl.unitTests;

import java.util.ArrayList;
import java.util.List;

import jp.ac.kobe_u.cs.prolog.lang.JavaObjectTerm;
import jp.ac.kobe_u.cs.prolog.lang.Term;
import jp.ac.kobe_u.cs.prolog.lang.VariableTerm;

import org.junit.Assert;
import org.junit.Test;

import edu.cmu.cs.erl.ERL;
import edu.cmu.cs.erl.ERLError;
import edu.cmu.cs.erl.ERLException;
import edu.cmu.cs.erl.Oracle;
import edu.cmu.cs.erl.TermBuilder;



public class ExistsTest {
	@Test
	public void sizeOneListTrue() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = (VariableTerm)TermBuilder.createVariableTerm();
		Term term1 = TermBuilder.createAtomicTerm(X);
		Term term2 = TermBuilder.createAtomicTerm("a");
		Term andTerm = TermBuilder.createAndTerm(term1, term2);
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("a");
		
		Term exists = TermBuilder.createExistsTerm(list,X,andTerm);
		List<ERLError> errors = ERL.runPredicate(oracle, exists, true);
		
		Assert.assertTrue(errors.isEmpty());
	}
	
	@Test
	public void sizeOneListFalse() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = (VariableTerm)TermBuilder.createVariableTerm();
		Term term1 = TermBuilder.createAtomicTerm(X);
		Term term2 = TermBuilder.createAtomicTerm("a");
		Term andTerm = TermBuilder.createAndTerm(term1, term2);
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("b");
		
		Term exists = TermBuilder.createExistsTerm(list,X,andTerm);
		List<ERLError> errors = ERL.runPredicate(oracle, exists, true);
		
		Assert.assertEquals(1, errors.size());
	}

	@Test
	public void sizeManyListOneTrue() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = (VariableTerm)TermBuilder.createVariableTerm();
		Term term1 = TermBuilder.createAtomicTerm(X);
		Term term2 = TermBuilder.createAtomicTerm("a");
		Term andTerm = TermBuilder.createAndTerm(term1, term2);
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("b");
		list.add("a");
		list.add("b");
		
		Term exists = TermBuilder.createExistsTerm(list,X,andTerm);
		List<ERLError> errors = ERL.runPredicate(oracle, exists, true);
		
		Assert.assertTrue(errors.isEmpty());
	}
	
	@Test
	public void sizeManyAllFailList() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = (VariableTerm)TermBuilder.createVariableTerm();
		Term term1 = TermBuilder.createAtomicTerm(X);
		Term term2 = TermBuilder.createAtomicTerm("a");
		Term andTerm = TermBuilder.createAndTerm(term1, term2);
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("b");
		list.add("b");
		list.add("b");
		
		Term exists = TermBuilder.createExistsTerm(list,X,andTerm);
		List<ERLError> errors = ERL.runPredicate(oracle, exists, true);
		
		//Assert.assertEquals(3, errors.size());
		Assert.assertEquals("b", errors.get(0).getOwner());
	}
	

	
	@Test
	public void nestedForAll() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = (VariableTerm)TermBuilder.createVariableTerm();
		VariableTerm Y = (VariableTerm)TermBuilder.createVariableTerm();
		Term term1 = TermBuilder.createAtomicTerm(X);
		Term term2 = TermBuilder.createAtomicTerm(Y);
		Term andTerm = TermBuilder.createAndTerm(term1, term2);
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("a");
		list.add("b");
		
		Term innerexistsTerm = TermBuilder.createExistsTerm(list,X,andTerm);
		Term outterexistsTerm = TermBuilder.createExistsTerm(list,Y,innerexistsTerm);
		List<ERLError> errors = ERL.runPredicate(oracle, outterexistsTerm, true);
		
		System.out.println("Delete this: size="+errors.size());
		/*Assert.assertEquals(4, errors.size());
		Assert.assertEquals("b", errors.get(0).getOwner());
		Assert.assertEquals("a", errors.get(1).getOwner());
		Assert.assertEquals("b", errors.get(2).getOwner());
		Assert.assertEquals("b", errors.get(3).getOwner());*/
		
	}
	
	@Test
	public void checkLazyLoading() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = oracle.getVariable("X");
		Term term1 = TermBuilder.createAtomicTerm(X);
		Term term2 = TermBuilder.createAtomicTerm("a");
		Term andTerm = TermBuilder.createAndTerm(term1, term2);
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("a");
		list.add("b");
		list.add("a");
		
		Term forAll = TermBuilder.createExistsLazyTerm(oracle,list,"X",andTerm);
		List<ERLError> errors = ERL.runPredicate(oracle, forAll, true);
		
		Assert.assertTrue(errors.isEmpty());
	}
	
	@Test
	public void checkLazyLoadingLastElement() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = oracle.getVariable("X");
		Term term1 = TermBuilder.createAtomicTerm(X);
		Term term2 = TermBuilder.createAtomicTerm("a");
		Term andTerm = TermBuilder.createAndTerm(term1, term2);
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("b");
		list.add("b");
		list.add("a");
		
		Term forAll = TermBuilder.createExistsLazyTerm(oracle,list,"X",andTerm);
		List<ERLError> errors = ERL.runPredicate(oracle, forAll, true);
		
		Assert.assertTrue(errors.isEmpty());
	}
	
	@Test
	public void checkLazyLoadingFalseAnd() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = oracle.getVariable("X");
		Term term1 = TermBuilder.createAtomicTerm(X);
		Term term2 = TermBuilder.createAtomicTerm("a");
		Term andTerm = TermBuilder.createAndTerm(term1, term2);
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("b");
		list.add("b");
		list.add("b");
		
		Term exists = TermBuilder.createExistsLazyTerm(oracle,list,"X",andTerm);
		List<ERLError> errors = ERL.runPredicate(oracle, exists, true);
		
		Assert.assertEquals(errors.size(), 1);
	}
	
	@Test
	public void checkLazyLoadingFalseImplies() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = oracle.getVariable("X");
		Term term1 = TermBuilder.createAtomicTerm("a");
		Term term2 = TermBuilder.createAtomicTerm(X);
		Term impliesTerm = TermBuilder.createImpliesTerm(term1, term2);
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("b");
		list.add("b");
		list.add("b");
		
		Term exists = TermBuilder.createExistsLazyTerm(oracle,list,"X",impliesTerm);
		List<ERLError> errors = ERL.runPredicate(oracle, exists, true);
		
		Assert.assertEquals(errors.size(), 1);
	}
	
	@Test
	public void checkLazyLoadingFalseExists() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = oracle.getVariable("X");
		VariableTerm Y = oracle.getVariable("Y");
		Term term1 = TermBuilder.createAtomicTerm(X);
		Term term2 = TermBuilder.createAtomicTerm(Y);
		Term andTerm = TermBuilder.createAndTerm(term1, term2);
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("b");
		list.add("b");
		
		
		Term exists = TermBuilder.createExistsLazyTerm(oracle,list,"X",andTerm);
		Term outexists = TermBuilder.createExistsLazyTerm(oracle,list,"Y",exists);
		List<ERLError> errors = ERL.runPredicate(oracle, outexists, true);
		
		Assert.assertEquals(errors.size(), 1);
	}
	
	@Test
	public void checkLazyLoadingTrueForall() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = oracle.getVariable("X");
		VariableTerm Y = oracle.getVariable("Y");
		Term term1 = TermBuilder.createAtomicTerm(X);
		Term term2 = TermBuilder.createAtomicTerm(Y);
		Term andTerm = TermBuilder.createAndTerm(term1, term2);
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("b");
		list.add("b");
		list.add("a");
		
		ArrayList<String> list2 = new ArrayList<String>();
		list.add("a");
		list.add("a");
		list.add("a");
		
		Term forall = TermBuilder.createForAllLazyTerm(oracle,list2,"X",andTerm);
		Term outexists = TermBuilder.createExistsLazyTerm(oracle,list,"Y",forall);
		List<ERLError> errors = ERL.runPredicate(oracle, outexists, true);
		
		Assert.assertEquals(errors.size(), 0);
	}

	@Test
	public void checkLazyLoadingEmpty() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = oracle.getVariable("X");
		Term term1 = TermBuilder.createAtomicTerm(X);
		Term term2 = TermBuilder.createAtomicTerm("a");
		Term andTerm = TermBuilder.createAndTerm(term1, term2);
		
		ArrayList<String> list = new ArrayList<String>();
		
		Term forAll = TermBuilder.createExistsLazyTerm(oracle,list,"X",andTerm);
		List<ERLError> errors = ERL.runPredicate(oracle, forAll, true);
		
		Assert.assertEquals(errors.size(), 1);
	}
	
	@Test
	public void checkLazyLoadingEmpty2() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = oracle.getVariable("X");
		Term term1 = TermBuilder.createAtomicTerm(X);
		
		ArrayList<String> list = new ArrayList<String>();
		
		Term exists = TermBuilder.createExistsLazyTerm(oracle,list,"X",term1);
		List<ERLError> errors = ERL.runPredicate(oracle, exists, true);
		
		Assert.assertEquals(errors.size(), 1);
	}

}
